$\forall$$i$:Id, $X$:Type, $p$:FinProbSpace, $x_{0}$:$X$, $P$:($X$$\rightarrow\mathbb{B}$).
\\[0ex]Normal($X$) $\Rightarrow$ (preinit1R\{x:ut2, a:ut2\}($i$; $X$; $p$; $x_{0}$; $P$) $\in$ Realizer)